1. Field of the Invention
This invention relates generally to verification of control system properties and, more particularly, to a method for infeasibility identification in timed automata which checks an abstract model of a real-time system against a Linear Temporal Logic specification and, if a counterexample is found, validates or invalidates the counterexample using negative cycle detection, identifies a minimal infeasible trace fragment, and refines the specification.
2. Discussion of the Related Art
Modern vehicles employ many types of embedded control systems, to improve the performance, comfort, and safety of the vehicles. Such control systems include engine controls, suspension controls, and steering controls, among many others. Real time systems are important for their use in verification of embedded automotive control systems, and control systems in other applications such as aircraft. Formal verification of a control system is proof that the system satisfies a given property under every possible condition. If verification is not possible, then a counterexample is provided—that is, a trajectory in which the given property fails.
Some existing verification approaches compute all reachable states until a fixed point is reached, or an undesirable state is reached. Other verification approaches work backwards from an undesirable state to find all states that could lead to it. These approaches do not scale well to large problem sizes, due to the exhaustive nature of the reachable state computation. This is because the computer memory required to run a formal verification grows exponentially with the number of variables in the control system state space. For the complex control systems which are typical of automotive applications, the number of variables involved makes traditional exhaustive verification approaches untenable, both in terms of computation time and memory space requirements.
Another verification approach has been proposed, where counterexample fragments are used to guide specification refinement for linear hybrid automata (LHA). However, there is an opportunity to make this approach more efficient for control systems modeled as timed automata (TA), which are a subset of LHA.